(declare-fun a () String)
(assert (str.in_re (str.++ "z" a) (re.++ (re.+ (re.++ (re.* (re.union (str.to_re "z") (re.++ (re.union (str.to_re (str.++ "z" "a")) (str.to_re "a")) (re.union (str.to_re "z") (str.to_re "b"))))) (re.union (str.to_re "b") (str.to_re "a")))) (str.to_re "b"))))
(assert (str.in_re (str.++ "z" a) (re.++ (re.* (re.union (str.to_re "z") (re.++ (re.union (str.to_re "b") (re.++ (re.* (re.union (str.to_re "z") (re.++ (re.union (str.to_re "b") (str.to_re "a")) (re.union (str.to_re "z") (str.to_re "b"))))) (re.++ (str.to_re "b") (re.* (str.to_re "b"))))) (re.union (str.to_re "z") (str.to_re "b"))))) (re.union (re.* (re.union (re.union (re.diff (re.range "a" "u") (re.++ (str.to_re "") (re.++ (re.* (re.union (str.to_re "z") (str.to_re "a"))) (str.to_re "b")))) (str.to_re "a")) (re.++ (str.to_re "b") (re.++ (re.* (str.to_re "b")) (re.union (str.to_re "z") (str.to_re "a")))))) (str.to_re "a")))))
(assert (not (str.in_re (str.++ "a" a) (re.++ (re.* (re.union re.allchar (re.++ (str.to_re "b") (re.++ (re.* (re.union re.all (str.to_re "a"))) (re.+ (re.range "a" "u")))))) (re.++ (re.++ (re.++ (re.* (re.union (str.to_re "z") (str.to_re "a"))) (str.to_re "b")) (re.++ (re.* (re.union (re.union (str.to_re "z") (str.to_re "a")) (re.++ (str.to_re "b") (re.++ (re.* (str.to_re "b")) (re.union (str.to_re "z") (str.to_re "a")))))) (re.++ (str.to_re "b") (re.* (str.to_re (str.substr (str.++ "a" a) 0 0)))))) (re.* (re.union (str.to_re "z") (str.to_re (str.++ "aa" a)))))))))
(check-sat)
